Termination Proof Script

• Consider the SCC {32,45}. There are no usable rules. By taking the AF π with π(2nd#) = π(mark) = 1 together with the lexicographic path order with empty precedence, rule 32 is weakly decreasing and rule 45 is strictly decreasing. There is one new SCC.
  • Consider the SCC {32}. By taking the AF π with π(2nd#) = 1 together with the lexicographic path order with empty precedence, rule 32 is strictly decreasing.


• Consider the SCC {33,46}. There are no usable rules. By taking the AF π with π(CONS) = π(mark) = 1 together with the lexicographic path order with empty precedence, rule 33 is weakly decreasing and rule 46 is strictly decreasing. There is one new SCC.
  • Consider the SCC {33}. By taking the AF π with π(CONS) = 1 together with the lexicographic path order with empty precedence, rule 33 is strictly decreasing.


• Consider the SCC {34,47}. There are no usable rules. By taking the AF π with π(FROM) = π(mark) = 1 together with the lexicographic path order with empty precedence, rule 34 is weakly decreasing and rule 47 is strictly decreasing. There is one new SCC.
  • Consider the SCC {34}. By taking the AF π with π(FROM) = 1 together with the lexicographic path order with empty precedence, rule 34 is strictly decreasing.


• Consider the SCC {35,48}. There are no usable rules. By taking the AF π with π(mark) = π(S) = 1 together with the lexicographic path order with empty precedence, rule 35 is weakly decreasing and rule 48 is strictly decreasing. There is one new SCC.
  • Consider the SCC {35}. By taking the AF π with π(S) = 1 together with the lexicographic path order with empty precedence, rule 35 is strictly decreasing.


• Consider the SCC {37,39,40,42,44}. There are no usable rules. By taking the AF π with π(2nd) = π(from) = π(PROPER) = π(s) = 1 together with the lexicographic path order with empty precedence, the rules in {37,42,44} are weakly decreasing and the rules in {39,40} are strictly decreasing. There is one new SCC.
  • Consider the SCC {37,42,44}. By taking the AF π with π(2nd) = π(from) = π(PROPER) = 1 together with the lexicographic path order with empty precedence, the rules in {37,42} are weakly decreasing and rule 44 is strictly decreasing. There is one new SCC.
    • Consider the SCC {37,42}. By taking the AF π with π(2nd) = π(PROPER) = 1 together with the lexicographic path order with empty precedence, rule 37 is weakly decreasing and rule 42 is strictly decreasing. There is one new SCC.
      • Consider the SCC {37}. By taking the AF π with π(PROPER) = 1 together with the lexicographic path order with empty precedence, rule 37 is strictly decreasing.


• Consider the SCC {25,27,29,31}. There are no usable rules. By taking the AF π with π(2nd) = π(ACTIVE) = π(cons) = π(from) = 1 together with the lexicographic path order with empty precedence, the rules in {25,27,29} are weakly decreasing and rule 31 is strictly decreasing. There is one new SCC.
  • Consider the SCC {25,27,29}. By taking the AF π with π(2nd) = π(ACTIVE) = π(cons) = 1 together with the lexicographic path order with empty precedence, the rules in {25,27} are weakly decreasing and rule 29 is strictly decreasing. There is one new SCC.
    • Consider the SCC {25,27}. By taking the AF π with π(2nd) = π(ACTIVE) = 1 and π(cons) = [1] together with the lexicographic path order with empty precedence, rule 25 is weakly decreasing and rule 27 is strictly decreasing. There is one new SCC.
      • Consider the SCC {25}. By taking the AF π with π(ACTIVE) = 1 together with the lexicographic path order with empty precedence, rule 25 is strictly decreasing.


• Consider the SCC {49,51}. The usable rules are {1-18}. By taking the AF π with π(2nd) = π(cons) = π(from) = π(s) = π(TOP) = 1 and π(active) = π(mark) = π(ok) = π(proper) = [ ] together with the lexicographic path order with precedence ok ≻ active ≻ mark ≻ proper, the rules in {3-18} are weakly decreasing and the rules in {1,2,49,51} are strictly decreasing.